Nuprl Lemma : inv_image_ind_a
9,38
postcript
pdf
T
:Type,
r
:(
T
T
),
S
:Type,
f
:(
S
T
).
WellFnd{i}(
T
;
x
,
y
.
r
(
x
,
y
))
WellFnd{i}(
S
;
x
,
y
.
r
(
f
(
x
),
f
(
y
)))
latex
ProofTree
Definitions
x
,
y
.
t
(
x
;
y
)
,
t
T
,
x
(
s1
,
s2
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
{
T
}
,
x
(
s
)
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
x
.
t
(
x
)
Lemmas
wellfounded
wf
origin
T:Type, r:(T
T
), S:Type, f:(ST).
WellFnd{i}(S;x,y.r(f(x),f(y)))
T:Type, r:(TT), S:Type, f:(ST).
WellFnd{i}(S;x,y.r(f(x),f(y)))
x,y. t(x;y)
T Qx:A. B(x)x. t(x)